$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $a$, $b$:$\mathbb{N}$, $x$, $z$:$T$.
\\[0ex]($x$ rel\_exp($T$;$R$;$a$+$b$) $z$) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. (($x$ rel\_exp($T$;$R$;$a$) $y$) \& ($y$ rel\_exp($T$;$R$;$b$) $z$)))